T:Type, L:(T List), x:T. (null(L))  ((x  L)) 

latex

Definitions	P  Q, x:A. B(x), , t  T, A, P & Q, P  Q, False, P  Q
Lemmas	l member wf, not wf, null wf, assert wf, nil member, false wf, not functionality wrt iff